/**
 * 
 */
package GSR.web;

import static constants.GTextbookConstants.language;

import java.util.Vector;
import java.util.regex.Matcher;
import java.util.regex.Pattern;

import javax.swing.JOptionPane;

import ui.view.LangWarningPane;


import com.maplesoft.externalcall.MapleException;
import com.maplesoft.openmaple.Engine;

/**
 * @author Franknew
 *
 */
public class Utility {
	public static String getFormalString4Multiple(String data,String name, String role){
		StringBuffer result = new StringBuffer(10);
		String HC=data;
		result.append("Problems(");
		int index = data.indexOf("<=>");
		if(index !=-1 ){
			//if the data is in the form in GDL
			if(data.indexOf("Problem")!=-1||data.indexOf("Proposition")!=-1){
				Vector<String> buf = generateTermSet(data);
				HC = deleteConfiguration(buf.get(3)) + "," + buf.get(4);
			}
			System.out.println(HC);
			
			index = HC.indexOf("<=>");
			String hypothesisString = HC.substring(0,index);
			String conclusionString = HC.substring(index+3,HC.length());
			
			result.append(getFormalString4Single(hypothesisString + "=>" +conclusionString, name+"_forward", role));
				
			System.out.println(hypothesisString);
			//the new conclusion is the last one in the hypothesis
			Vector<String> H = generateTermSet("f("+hypothesisString+")");
			String newConclusion = H.get(H.size()-1);
			StringBuffer buf = new StringBuffer(20);
			for(int i = 1; i < H.size()-1; i++){
				buf.append(H.get(i)+",");
			}
			buf.append(conclusionString+"=>"+newConclusion);
			
			result.append(","+getFormalString4Single(buf.toString(),name+"_backward",role)+")");
			
		}else{
			//index = data.indexOf("=>");
			//if(index!=-1){
				//in the form of .... A => B
				//result.append(getFormalString4Single(data,name,role)+")");
			//}else{
				//there is no <=> or =>
				result.append(getFormalString4Single(data,name,role)+")");
			//}
		}
		
		return result.toString();
	}
	
	
	
	public static String getFormalString4Single(String data, String name, String role){
		StringBuffer result = new StringBuffer(10);
		int index = data.indexOf("=>");
		if(index !=-1){
			String hypothesisString = data.substring(0,index);
			String conclusionString = data.substring(index+2,data.length());
			StringBuffer buf = new StringBuffer(100);
			buf.append("assume(");
			buf.append(hypothesisString+")");
			StringBuffer buf1 = new StringBuffer(100);
			buf1.append("show(");
			buf1.append(conclusionString+")");				
			result.append("Problem(" + name + "," + role + "," + buf.toString() + "," + buf1.toString() +")");
			
		}else{
			//there is no =>, then it must be in the formal statement of GDL
			Vector<String> H = generateTermSet(data);
			System.out.println(H.size());
			String hypothesis = H.get(3).replaceFirst("configuration", "assume");
			String conclusion = "show(" + H.get(4) + ")";
			result.append("Problem(" + name + "," + role + "," + hypothesis + "," + conclusion +")");
		}
		return result.toString();
	}
	
	
	public static String deleteConfiguration(String input){
		StringBuffer result = new StringBuffer(100);
		int index = input.trim().indexOf("configuration");
		if(index !=-1){
			Vector<String> H = generateTermSet(input);
			for(int i =1;i<H.size();i++){
				result.append(deleteConfiguration(H.get(i))+",");
			}
			result.replace(result.lastIndexOf(","), result.length(), "");
		}else{
			result.append(input);
		}
		
		
		return result.toString();
	}
	
	public static Vector<String> generateTermSet(String test){
	      int[][] t = matchPairs(test);
	    //  System.out.println("The pairs of parentheses are: ");
	      //for(int i = 0; i < t.length; i++){
	     //    System.out.println("start " + t[i][0] + " end "+ t[i][1]);
	      //}
	      Vector<String> term = new Vector<String>(5,5);
	      term.add(test.substring(0,t[0][0]));
	      int begin = t[0][0]+1;
	      int over = 0;
	      while(begin < test.length()){
	         for(int point = begin;point < test.length();point++){
	            if(test.charAt(point)=='('||test.charAt(point)=='（'){
	               for(int y = 0;y < t.length;y++){
	                  if(t[y][0] == point)
	                    { 
	                    point = t[y][1]+1;
	                  //  System.out.println("The mark of extracted term: "+ t[y][1]);
	                    break;
	                    }
	                                          
	               }
	            }
	            if(test.charAt(point)==','||test.charAt(point)=='；'||test.charAt(point)==')'||test.charAt(point)=='）'){
	               over = point;
	               break;
	            }
	            
	         }  
	            
	         //È·¶¨ÖÕµã
	         if(begin!=over){
	         term.add(test.substring(begin,over));
	         System.out.println("Start: " + begin + "||Over: " + over);
	         }									//ÌáÈ¡Ïî
	         begin = over+1;                                //ÖØÐÂÌáÈ¡ 


	        
	       
	         
	      }
	    //  System.out.println("The size of termSet: " + term.size());
	     // System.out.println("The term in termSet are:\n");
	     // for(int index = 0; index < term.size();index++){        
	      //  System.out.println(index + " " + term.get(index));
	      //}
	      return term;
	   }
	
	public static int[][] matchPairs(String test){
	      
	      Vector<Integer> textBone = new Vector<Integer>(10,10);
	      String regEx = "\\(|\\)|\\（|\\）";
	      Pattern pattern = Pattern.compile(regEx);
	      Matcher m = pattern.matcher(test);
	      
	     while( m.find() ){
	   //   System.out.println("Parentheses found at Start: "+m.start());
	      textBone.add(m.start());
	     }
	     
	     int[][] pairs = new int[textBone.size()/2][2];
	     int count = 0;
	     int start = 0;
	     int end = 0;
	     int n = 0;
	    
	    for(int j = 0; j < textBone.size(); j++){
	      start = textBone.get(j);
	      if (textBone.get(j)==0)
	         continue;
	      else{      
	         int t = j;
	         do {
	            if (test.charAt(textBone.get(t))=='('||test.charAt(textBone.get(t))=='（'){
	               count++;
	               t++;
	            }
	            if (test.charAt(textBone.get(t))==')'||test.charAt(textBone.get(t))=='）'){
	               count--;
	               t++;
	            }   
	         }while(count!=0);
	         end = textBone.get(t-1);
	         textBone.set(t-1,0);
	         t++;
	         pairs[n][0] = start;  //½«Åä¶ÔµÄ½á¹ûÐ´Èë¶þÎ»Êý×é
	         pairs[n][1] = end;
	         n++;
	      }
	   }
	  return pairs;
	}
	
	public static Engine buildEngine4Maple(CallBacks callback){
		
		 Engine engine;
		 
		  /* build the command line arguments for Maple */
			String a[];
	        a = new String[1];
	        a[0] = "java";
	        
	        try
	        {
	            /* start the Maple session.  Use the Default EngineCallBacks. 
	             * the text Output will be directed to System.out */
	            engine = new Engine(a,callback,null, null );
	            engine.evaluate( "with(geother);");
	            return engine;
	        }
	        catch ( MapleException e1 )
	        {
	            /* if an error occurs, exit */
	        	LangWarningPane.showMessageDialog(null,"Cannot connect to Maple！Cannot use GEOTHER！", "无法连接到Maple！无法使用GEOTHER！", "Auto Proving Disabled", "自动证明不可用", JOptionPane.ERROR_MESSAGE, language.getNum());			
	        	System.out.println(e1);
	            System.out.println( "An exception occured\n" );
	            return null;
	        }  
	}
	
}
